Armin Biere
46 publications
8 venues
H Index 22
Affiliation
Universit t Freiburg, GermanyJohannes Kepler University of Linz, Austria
Links
DBLPGoogle Scholar
ORCID- https://cca.informatik.uni-freiburg.de/biere/
- https://zbmath.org/authors/?q=ai:biere.armin
- https://www.wikidata.org/entity/Q687404
- https://www.researcherid.com/rid/C-4438-2013
- http://isni.org/isni/0000000078579332
- https://id.loc.gov/authorities/names/no2006075968
- https://d-nb.info/gnd/115751823
- https://mathgenealogy.org/id.php?id=111891
| Name | Venue | Year | citations |
|---|---|---|---|
CadiBack: Extracting Backbones with CaDiCaL.
|
SAT | 2023 | 0 |
| Faster LRAT Checking Than Solving with CaDiCaL.
|
SAT | 2023 | 0 |
| IPASIR-UP: User Propagators for CDCL.
|
SAT | 2023 | 0 |
| Migrating Solver State.
|
SAT | 2022 | 0 |
| Better Decision Heuristics in CDCL through Local Search and Target Phases.
|
JAIR | 2022 | 2 |
| Efficient All-UIP Learned Clause Minimization.
|
SAT | 2021 | 3 |
| Non-clausal Redundancy Properties.
|
CADE | 2021 | 3 |
| XOR Local Search for Boolean Brent Equations.
|
SAT | 2021 | 0 |
| Decomposition Strategies to Count Integer Solutions over Linear Constraints.
|
IJCAI | 2021 | 0 |
| Four Flavors of Entailment.
|
SAT | 2020 | 2 |
| Duplex Encoding of Staircase At-Most-One Constraints for the Antibandwidth Problem.
|
CPAIOR | 2020 | 2 |
| Distributed Cube and Conquer with Paracooba.
|
SAT | 2020 | 11 |
| Incremental Inprocessing in SAT Solving.
|
SAT | 2019 | 26 |
| Backing Backtracking.
|
SAT | 2019 | 18 |
| Blocked Clauses in First-Order Logic.
|
LPAR | 2017 | 12 |
| Short Proofs Without New Variables.
|
CADE | 2017 | 32 |
| Blockedness in Propositional Logic: Are You Satisfied With Your Neighborhood?
|
IJCAI | 2017 | 3 |
| SAT Race 2015.
|
Artificial Intelligence | 2016 | 52 |
| Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination.
|
LPAR | 2015 | 34 |
| Clause Elimination for SAT and QSAT.
|
JAIR | 2015 | 63 |
| Compositional Propositional Proofs.
|
LPAR | 2015 | 11 |
| Stochastic Local Search for Satisfiability Modulo Theories.
|
AAAI | 2015 | 34 |
| Evaluating CDCL Variable Scoring Schemes.
|
SAT | 2015 | 78 |
| Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask).
|
SAT | 2014 | 14 |
| Detecting Cardinality Constraints in CNF.
|
SAT | 2014 | 45 |
| Improving Implementation of SLS Solvers for SAT and New Heuristics for k-SAT with Long Clauses.
|
SAT | 2014 | 15 |
| Blocked Clause Decomposition.
|
LPAR | 2013 | 19 |
| : A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into.
|
CADE | 2013 | 4 |
| Factoring Out Assumptions to Speed Up MUS Extraction.
|
SAT | 2013 | 45 |
| Revisiting Hyper Binary Resolution.
|
CPAIOR | 2013 | 19 |
| Concurrent Cube-and-Conquer - (Poster Presentation).
|
SAT | 2012 | 7 |
| Resolution-Based Certificate Extraction for QBF - (Tool Presentation).
|
SAT | 2012 | 56 |
| Failed Literal Detection for QBF.
|
SAT | 2011 | 21 |
| Efficient CNF Simplification Based on Binary Implication Graphs.
|
SAT | 2011 | 65 |
| Blocked Clause Elimination for QBF.
|
CADE | 2011 | 122 |
| Reconstructing Solutions after Blocked Clause Elimination.
|
SAT | 2010 | 23 |
| Automated Testing and Debugging of SAT and QBF Solvers.
|
SAT | 2010 | 93 |
| Integrating Dependency Schemes in Search-Based QBF Solvers.
|
SAT | 2010 | 57 |
| A Compact Representation for Syntactic Dependencies in QBFs.
|
SAT | 2009 | 18 |
| Minimizing Learned Clauses.
|
SAT | 2009 | 117 |
| Nenofex: Expanding NNF for QBF Solving.
|
SAT | 2008 | 50 |
| Adaptive Restart Strategies for Conflict Driven SAT Solvers.
|
SAT | 2008 | 112 |
| A First Step Towards a Unified Proof Checker for QBF.
|
SAT | 2007 | 55 |
| Extended Resolution Proofs for Symbolic SAT Solving with Quantification.
|
SAT | 2006 | 41 |
| Effective Preprocessing in SAT Through Variable and Clause Elimination.
|
SAT | 2005 | 701 |
| Resolve and Expand.
|
SAT | 2004 | 294 |